T:Type, eq, le:(TT), op:(TTT), id:T, inv:(TT).
IsEqFun(T;eq)
 Assoc(T;op)
 Ident(T;op;id)
 Inverse(T;op;id;inv)
 (<T, eq, le, op, id, inv>  Group{i}) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), GrpSig, |g|, =, *, e, ~, Mon, Group{i}
Definitions	t  T, P  Q, x:A. B(x), t.2, t.1, ~, e, *, |g|, Group{i}, =, P & Q, Mon, GrpSig, IsMonoid(T;op;id),
Lemmas	bool wf, eqfun p wf, assoc wf, ident wf, inverse wf, grp inv wf, grp id wf, grp op wf, grp car wf, grp eq wf, monoid p wf